package kodkod.analysis;

import java.util.ArrayList;
import kodkod.ast.*;
import kodkod.ast.operator.ExprCompOperator;
import kodkod.ast.operator.FormulaOperator;

public class FormulaAnalyzer {
	
	Formula formula;
	
	ArrayList<FormulaAnalyzer> children = new ArrayList<FormulaAnalyzer>();
	enum Op {
		NONE, TRUE, FALSE, AND, OR, IMPLIES, IFF, NOT, EQUIV, SUBSET, INT, MULT, QUANT, RP
	}
	Op type = Op.NONE;
	
	public FormulaAnalyzer(Formula formula) {
		this.formula = formula;
		
		if (formula instanceof BinaryFormula) {
			BinaryFormula f = (BinaryFormula)formula;
			if (f.op().equals(FormulaOperator.AND)) {
				type = Op.AND;
			} else if (f.op().equals(FormulaOperator.OR)) {
				type = Op.OR;
			} else if (f.op().equals(FormulaOperator.IMPLIES)) {
				type = Op.IMPLIES;
			} else if (f.op().equals(FormulaOperator.IFF)) {
				type = Op.IFF;
			}
			children.add(new FormulaAnalyzer(f.left()));
			children.add(new FormulaAnalyzer(f.right()));
		} else if (formula instanceof NaryFormula) {
			NaryFormula f = (NaryFormula)formula;
			if (f.op().equals(FormulaOperator.AND)) {
				type = Op.AND;
			} else if (f.op().equals(FormulaOperator.OR)) {
				type = Op.OR;
			}
			for (Formula child : f) {
				children.add(new FormulaAnalyzer(child));
			}
		} else if (formula instanceof NotFormula) {
			NotFormula f = (NotFormula)formula;
			type = Op.NOT;
			children.add(new FormulaAnalyzer(f.formula()));
		} else if (formula instanceof ComparisonFormula) {
			ComparisonFormula f = (ComparisonFormula)formula;
			if (f.op().equals(ExprCompOperator.EQUALS)) {
				type = Op.EQUIV;
			} else {
				type = Op.SUBSET;
			}
		} else if (formula instanceof ConstantFormula) {
			ConstantFormula f = (ConstantFormula)formula;
			type = f.booleanValue() ? Op.TRUE : Op.FALSE;
		} else if (formula instanceof IntComparisonFormula) {
			IntComparisonFormula f = (IntComparisonFormula)formula;
			type = Op.INT;
		} else if (formula instanceof MultiplicityFormula) {
			MultiplicityFormula f = (MultiplicityFormula)formula;
			type = Op.MULT;
		} else if (formula instanceof QuantifiedFormula) {
			QuantifiedFormula f = (QuantifiedFormula)formula;
			type = Op.QUANT;
		} else if (formula instanceof RelationPredicate) {
			RelationPredicate f = (RelationPredicate)formula;
			type = Op.RP;
		}
	}
}
